es:ES, C, T:Type, R1, R2:(CE), decodes1:(i:Ce:{x:E| R1(i,x)} state@loc(e)T),
decodes2:(i:Ce:{x:E| R2(i,x)} state@loc(e)T).
(i:C, e:E. Dec(R1(i,e)))
 (i:C, e:E. Dec(R2(i,e)))
 (i:C, e:E. (R1(i,e) & R2(i,e)))
 (decodes:i:Ce:{x:E| (R1(i,x))  (R2(i,x))} state@loc(e)T
 ((i:C, e:{x:E| (R1(i,x))  (R2(i,x))} , st:state@loc(e).
 (((R1(i,e))  (decodes(i,e,st) = decodes1(i,e,st)))
 (& ((R2(i,e))  (decodes(i,e,st) = decodes2(i,e,st))))) 

latex

Definitions	P  Q, P  Q, x:A. B(x), s = t, left + right, A, P & Q, x:A  B(x), Dec(P), {x:A| B(x)} , f(a), state@i, loc(e), x:AB(x), E, x:A. B(x), , Type, t  T, ES, x.A(x), if p:P then A(p) else B fi , t.1, b, False, <a, b>
Lemmas	event system wf, es-E wf, es-loc wf, es-state wf, decidable wf, not wf